%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Lanzarote ama a la reina Ginebra. El Rey Arturo y Lanzarote son amigos. Los
% amigos de Lanzarote odian a aquellos a quienes Lanzarote ama. Por tanto el
% Rey Arturo odia a la reina Ginebra." 

%==============================================================================
% Formalización
%==============================================================================

set(binary_res).
set(very_verbose).

formula_list(sos).

% Lanzarote ama a la reina Ginebra.
  ama(Lanzarote,RGinebra).

% El Rey Arturo y Lanzarote son amigos.
  amigos(RArturo,Lanzarote).

% La propiedad 'amigos' es reflexiva.
  all x y (amigos(x,y) -> amigos(y,x)).

% Los amigos de Lanzarote odian a aquellos a quienes Lanzarote ama.
  all x y (amigos(Lanzarote,x) & ama(Lanzarote,y) -> odia(x,y)).

% Conclusión: el Rey Arturo odia a la reina Ginebra.
  - odia(RArturo,RGinebra).

end_of_list.

%==============================================================================
